/* Benchmarks for the PionterC verifier. */

// clear a list

struct list 
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==null) ||
  @               (({l}) && list(l->next))
  @ in  list(l)
  @ end
  @*/
void clearList(struct list * l)
{
  struct list * p;
  
  p=l;
  //p->next = null;
  
  if (p==null)
      return;
  else
  {
    while(p!=null) /*@ (({p, l}) && list(l->next))
                     @ || ({p}N)
                     @*/  
      { //free (p);
      l = l->next;
      free (p);
      //free (p);
      p = l;
      // l= p;
      //p->next = null;
    }
    //free (p);
    return;
 }

}
/*@ */ 
